Nuprl Definition : princ_ideal
13,42
postcript
pdf
(
a
)
r
(
c
) ==
b
:|
r
|. (
c
= (
a
*
b
))
latex
clarification:
(
a
)
r
(
c
) ==
b
:|
r
|. (
c
= (
a
(*
r
)
b
)
|
r
|)
latex
Up
rings
1
Wellformedness Lemmas
princ
ideal
wf
Definitions
x
.
A
(
x
)
,
x
:
A
.
B
(
x
)
,
s
=
t
,
|
r
|
,
x
f
y
,
*
origin
b:|r|. (c = (a * b))
b:|r|. (c = (a (*r) b) 
|r|) b:|r|. (c = (a * b))
b:|r|. (c = (a (*r) b) |r|) 
x.A(x)x:A. B(x)